0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 87 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 1 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 UsableRulesReductionPairsProof (⇔, 82 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
orderedB_in_g([]) → orderedB_out_g([])
orderedB_in_g(.(T3, [])) → orderedB_out_g(.(T3, []))
orderedB_in_g(.(0, .(T15, T10))) → U2_g(T15, T10, orderedB_in_g(.(T15, T10)))
orderedB_in_g(.(s(T20), .(T21, T10))) → U3_g(T20, T21, T10, lessA_in_gg(T20, T21))
lessA_in_gg(0, s(T30)) → lessA_out_gg(0, s(T30))
lessA_in_gg(s(T35), s(T36)) → U1_gg(T35, T36, lessA_in_gg(T35, T36))
U1_gg(T35, T36, lessA_out_gg(T35, T36)) → lessA_out_gg(s(T35), s(T36))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → orderedB_out_g(.(s(T20), .(T21, T10)))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → U4_g(T20, T21, T10, orderedB_in_g(.(T21, T10)))
U4_g(T20, T21, T10, orderedB_out_g(.(T21, T10))) → orderedB_out_g(.(s(T20), .(T21, T10)))
U2_g(T15, T10, orderedB_out_g(.(T15, T10))) → orderedB_out_g(.(0, .(T15, T10)))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
orderedB_in_g([]) → orderedB_out_g([])
orderedB_in_g(.(T3, [])) → orderedB_out_g(.(T3, []))
orderedB_in_g(.(0, .(T15, T10))) → U2_g(T15, T10, orderedB_in_g(.(T15, T10)))
orderedB_in_g(.(s(T20), .(T21, T10))) → U3_g(T20, T21, T10, lessA_in_gg(T20, T21))
lessA_in_gg(0, s(T30)) → lessA_out_gg(0, s(T30))
lessA_in_gg(s(T35), s(T36)) → U1_gg(T35, T36, lessA_in_gg(T35, T36))
U1_gg(T35, T36, lessA_out_gg(T35, T36)) → lessA_out_gg(s(T35), s(T36))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → orderedB_out_g(.(s(T20), .(T21, T10)))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → U4_g(T20, T21, T10, orderedB_in_g(.(T21, T10)))
U4_g(T20, T21, T10, orderedB_out_g(.(T21, T10))) → orderedB_out_g(.(s(T20), .(T21, T10)))
U2_g(T15, T10, orderedB_out_g(.(T15, T10))) → orderedB_out_g(.(0, .(T15, T10)))
ORDEREDB_IN_G(.(0, .(T15, T10))) → U2_G(T15, T10, orderedB_in_g(.(T15, T10)))
ORDEREDB_IN_G(.(0, .(T15, T10))) → ORDEREDB_IN_G(.(T15, T10))
ORDEREDB_IN_G(.(s(T20), .(T21, T10))) → U3_G(T20, T21, T10, lessA_in_gg(T20, T21))
ORDEREDB_IN_G(.(s(T20), .(T21, T10))) → LESSA_IN_GG(T20, T21)
LESSA_IN_GG(s(T35), s(T36)) → U1_GG(T35, T36, lessA_in_gg(T35, T36))
LESSA_IN_GG(s(T35), s(T36)) → LESSA_IN_GG(T35, T36)
U3_G(T20, T21, T10, lessA_out_gg(T20, T21)) → U4_G(T20, T21, T10, orderedB_in_g(.(T21, T10)))
U3_G(T20, T21, T10, lessA_out_gg(T20, T21)) → ORDEREDB_IN_G(.(T21, T10))
orderedB_in_g([]) → orderedB_out_g([])
orderedB_in_g(.(T3, [])) → orderedB_out_g(.(T3, []))
orderedB_in_g(.(0, .(T15, T10))) → U2_g(T15, T10, orderedB_in_g(.(T15, T10)))
orderedB_in_g(.(s(T20), .(T21, T10))) → U3_g(T20, T21, T10, lessA_in_gg(T20, T21))
lessA_in_gg(0, s(T30)) → lessA_out_gg(0, s(T30))
lessA_in_gg(s(T35), s(T36)) → U1_gg(T35, T36, lessA_in_gg(T35, T36))
U1_gg(T35, T36, lessA_out_gg(T35, T36)) → lessA_out_gg(s(T35), s(T36))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → orderedB_out_g(.(s(T20), .(T21, T10)))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → U4_g(T20, T21, T10, orderedB_in_g(.(T21, T10)))
U4_g(T20, T21, T10, orderedB_out_g(.(T21, T10))) → orderedB_out_g(.(s(T20), .(T21, T10)))
U2_g(T15, T10, orderedB_out_g(.(T15, T10))) → orderedB_out_g(.(0, .(T15, T10)))
ORDEREDB_IN_G(.(0, .(T15, T10))) → U2_G(T15, T10, orderedB_in_g(.(T15, T10)))
ORDEREDB_IN_G(.(0, .(T15, T10))) → ORDEREDB_IN_G(.(T15, T10))
ORDEREDB_IN_G(.(s(T20), .(T21, T10))) → U3_G(T20, T21, T10, lessA_in_gg(T20, T21))
ORDEREDB_IN_G(.(s(T20), .(T21, T10))) → LESSA_IN_GG(T20, T21)
LESSA_IN_GG(s(T35), s(T36)) → U1_GG(T35, T36, lessA_in_gg(T35, T36))
LESSA_IN_GG(s(T35), s(T36)) → LESSA_IN_GG(T35, T36)
U3_G(T20, T21, T10, lessA_out_gg(T20, T21)) → U4_G(T20, T21, T10, orderedB_in_g(.(T21, T10)))
U3_G(T20, T21, T10, lessA_out_gg(T20, T21)) → ORDEREDB_IN_G(.(T21, T10))
orderedB_in_g([]) → orderedB_out_g([])
orderedB_in_g(.(T3, [])) → orderedB_out_g(.(T3, []))
orderedB_in_g(.(0, .(T15, T10))) → U2_g(T15, T10, orderedB_in_g(.(T15, T10)))
orderedB_in_g(.(s(T20), .(T21, T10))) → U3_g(T20, T21, T10, lessA_in_gg(T20, T21))
lessA_in_gg(0, s(T30)) → lessA_out_gg(0, s(T30))
lessA_in_gg(s(T35), s(T36)) → U1_gg(T35, T36, lessA_in_gg(T35, T36))
U1_gg(T35, T36, lessA_out_gg(T35, T36)) → lessA_out_gg(s(T35), s(T36))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → orderedB_out_g(.(s(T20), .(T21, T10)))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → U4_g(T20, T21, T10, orderedB_in_g(.(T21, T10)))
U4_g(T20, T21, T10, orderedB_out_g(.(T21, T10))) → orderedB_out_g(.(s(T20), .(T21, T10)))
U2_g(T15, T10, orderedB_out_g(.(T15, T10))) → orderedB_out_g(.(0, .(T15, T10)))
LESSA_IN_GG(s(T35), s(T36)) → LESSA_IN_GG(T35, T36)
orderedB_in_g([]) → orderedB_out_g([])
orderedB_in_g(.(T3, [])) → orderedB_out_g(.(T3, []))
orderedB_in_g(.(0, .(T15, T10))) → U2_g(T15, T10, orderedB_in_g(.(T15, T10)))
orderedB_in_g(.(s(T20), .(T21, T10))) → U3_g(T20, T21, T10, lessA_in_gg(T20, T21))
lessA_in_gg(0, s(T30)) → lessA_out_gg(0, s(T30))
lessA_in_gg(s(T35), s(T36)) → U1_gg(T35, T36, lessA_in_gg(T35, T36))
U1_gg(T35, T36, lessA_out_gg(T35, T36)) → lessA_out_gg(s(T35), s(T36))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → orderedB_out_g(.(s(T20), .(T21, T10)))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → U4_g(T20, T21, T10, orderedB_in_g(.(T21, T10)))
U4_g(T20, T21, T10, orderedB_out_g(.(T21, T10))) → orderedB_out_g(.(s(T20), .(T21, T10)))
U2_g(T15, T10, orderedB_out_g(.(T15, T10))) → orderedB_out_g(.(0, .(T15, T10)))
LESSA_IN_GG(s(T35), s(T36)) → LESSA_IN_GG(T35, T36)
LESSA_IN_GG(s(T35), s(T36)) → LESSA_IN_GG(T35, T36)
From the DPs we obtained the following set of size-change graphs:
ORDEREDB_IN_G(.(s(T20), .(T21, T10))) → U3_G(T20, T21, T10, lessA_in_gg(T20, T21))
U3_G(T20, T21, T10, lessA_out_gg(T20, T21)) → ORDEREDB_IN_G(.(T21, T10))
ORDEREDB_IN_G(.(0, .(T15, T10))) → ORDEREDB_IN_G(.(T15, T10))
orderedB_in_g([]) → orderedB_out_g([])
orderedB_in_g(.(T3, [])) → orderedB_out_g(.(T3, []))
orderedB_in_g(.(0, .(T15, T10))) → U2_g(T15, T10, orderedB_in_g(.(T15, T10)))
orderedB_in_g(.(s(T20), .(T21, T10))) → U3_g(T20, T21, T10, lessA_in_gg(T20, T21))
lessA_in_gg(0, s(T30)) → lessA_out_gg(0, s(T30))
lessA_in_gg(s(T35), s(T36)) → U1_gg(T35, T36, lessA_in_gg(T35, T36))
U1_gg(T35, T36, lessA_out_gg(T35, T36)) → lessA_out_gg(s(T35), s(T36))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → orderedB_out_g(.(s(T20), .(T21, T10)))
U3_g(T20, T21, T10, lessA_out_gg(T20, T21)) → U4_g(T20, T21, T10, orderedB_in_g(.(T21, T10)))
U4_g(T20, T21, T10, orderedB_out_g(.(T21, T10))) → orderedB_out_g(.(s(T20), .(T21, T10)))
U2_g(T15, T10, orderedB_out_g(.(T15, T10))) → orderedB_out_g(.(0, .(T15, T10)))
ORDEREDB_IN_G(.(s(T20), .(T21, T10))) → U3_G(T20, T21, T10, lessA_in_gg(T20, T21))
U3_G(T20, T21, T10, lessA_out_gg(T20, T21)) → ORDEREDB_IN_G(.(T21, T10))
ORDEREDB_IN_G(.(0, .(T15, T10))) → ORDEREDB_IN_G(.(T15, T10))
lessA_in_gg(0, s(T30)) → lessA_out_gg(0, s(T30))
lessA_in_gg(s(T35), s(T36)) → U1_gg(T35, T36, lessA_in_gg(T35, T36))
U1_gg(T35, T36, lessA_out_gg(T35, T36)) → lessA_out_gg(s(T35), s(T36))
ORDEREDB_IN_G(.(s(T20), .(T21, T10))) → U3_G(T21, T10, lessA_in_gg(T20, T21))
U3_G(T21, T10, lessA_out_gg) → ORDEREDB_IN_G(.(T21, T10))
ORDEREDB_IN_G(.(0, .(T15, T10))) → ORDEREDB_IN_G(.(T15, T10))
lessA_in_gg(0, s(T30)) → lessA_out_gg
lessA_in_gg(s(T35), s(T36)) → U1_gg(lessA_in_gg(T35, T36))
U1_gg(lessA_out_gg) → lessA_out_gg
lessA_in_gg(x0, x1)
U1_gg(x0)
The following rules are removed from R:
ORDEREDB_IN_G(.(s(T20), .(T21, T10))) → U3_G(T21, T10, lessA_in_gg(T20, T21))
U3_G(T21, T10, lessA_out_gg) → ORDEREDB_IN_G(.(T21, T10))
ORDEREDB_IN_G(.(0, .(T15, T10))) → ORDEREDB_IN_G(.(T15, T10))
Used ordering: POLO with Polynomial interpretation [POLO]:
lessA_in_gg(0, s(T30)) → lessA_out_gg
lessA_in_gg(s(T35), s(T36)) → U1_gg(lessA_in_gg(T35, T36))
U1_gg(lessA_out_gg) → lessA_out_gg
POL(.(x1, x2)) = 2·x1 + 2·x2
POL(0) = 1
POL(ORDEREDB_IN_G(x1)) = x1
POL(U1_gg(x1)) = 2·x1
POL(U3_G(x1, x2, x3)) = 2·x1 + 2·x2 + x3
POL(lessA_in_gg(x1, x2)) = x1 + 2·x2
POL(lessA_out_gg) = 1
POL(s(x1)) = 2·x1
lessA_in_gg(x0, x1)
U1_gg(x0)